<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
  <head>
    <meta content="text/html; charset=ISO-8859-1" http-equiv="content-type">
    <title>mmj2 Proof Assistant
    </title></head>
<body style="color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);" alink="#000088" link="#0000ff" vlink="#ff0000">

<pre style="font-weight: bold;"><big><big><big><big><small><span style="text-decoration: underline;">mmj2 Proof Assistant</span></small><br></big></big></big></big><br>(back to <a href="Start.html">Start.html</a>)<br></pre><big>The </big><a style="font-weight: bold;" href="Start.html">Start.html</a><big>
diagram shows "mmj2 Proof Asst" at the center, but the object in the
center of the diagram actually consists of more than just the main
(server) Proof Assistant program. <br>
<br>
Before the Proof Assistant is triggered, the input <a href="%5C..%5C..%5Cmmj2jar%5CAnnotatedRunParms.txt">RunParms.txt file</a> is processed and actions are taken accordingly. Then, if there are no serious errors and the input <a href="mmMetamathFile.html">Metamath .mm database file</a> has been successfully parsed, the main Proof Assistant program is called. <br>
<br>
From the user's perspective, the main Proof Assistant program is "management". It receives requests, primarily from the <a href="mmj2PAGUI.html">Proof Assistant GUI</a> screen, calls other programs as needed to satisfy the requests, and send the results back, along with any error messages. </big><br>
<pre style="font-weight: bold;">(back to <a href="Start.html">Start.html</a>)</pre>


</body></html>